\setlength{\columnsep}{7mm}
\section{Case Study}
In this section we analyze the case study \textit{OrderedPair}. This example is defined as 
a program implemented in Java language. 
Below, we present the $OrderedPair.java$ source. 



\begin{multicols}{2}

\begin{verbatim}
public class OrderedPair {
 int x,y;
 int oldx,oldy;

/*@
  @ ensures x == a;
  @ ensures oldx == a;
  @ ensures y == b;
  @ ensures oldy == b;  
  @*/

public void OrderedPair(int a, int b) {
// constructor
}

/*@
  @ ensures x == v;
  @ ensures oldx == \old(x);
  @*/

public void setx(int v) {
 this.oldx=this.x;
 this.x= v;
}

/*@
  @ ensures y == v;
  @ ensures oldy == \old(y);
  @*/

public void sety(int v) {
 this.oldy=this.y;
 this.y= v;
}


/*@
  @ ensures oldx == v;
  @*/

public void setoldx(int v) {
 this.oldx=v;
}


/*@
  @ ensures oldy == v;
  @*/

public void setoldy(int v) {
 this.oldy=v;
}


public int gety() {
 return (this.y);
}

public int getx() {
 return (this.x);
}


public int getoldy() {
 return (this.oldy);
}

public int getoldx() {
 return (this.oldx);
}


/*@
  @ ensures x == \old(y);
  @ ensures y == \old(x);
  @*/

 public void swap() {
  int a;
  this.oldx=x;
  this.oldy=y;
  a = this.x;
  this.x=this.y;
  this.y=a;
 }
  
}

\end{verbatim}


\end{multicols} 
The  java class  $OrderedPair.java$ model oredered pairs. 
%Los atributos x e y modelan el estado de las componentes de un par ordenado. Los atributos oldx y oldy el estado previo a la modificacion de las componenetes x e y .
The $x$ and $y$ attributes are the components of the ordered pair.
The  $oldy$  and $oldx$ attributes model the previous state to a modification of x and y respectively.
%La clase define los metodos gets y sets de cada atributo. Se define un metodo swap que permite intercambiar los valores de x e y. 
Besides to gets and sets methods, the class has the method $swap$ that allows to exchange x and y values​​.
%Para la definicion de los contratos los metodo de la clase utilizmos el lenguaje de especificación  de interfaz de comportamiento para módulos Java JML CITA.
Contracts are written in the specification language interface behavior for Java modules JML CITA.
%Las clausulas $ensures$ y $requires$ de $JML$  definen las pre y post condiciones respectivamente. 
The $ensures$ and $requires$ keywords of $JML$ define the pre-condition and post-condition respectively. 
%En este ejemplo la clausula $requires$ no se ha utilizado debido a que la pre-condicion para cada metodo es difinida como True por defecto.
In this example $requires$ keyword has not been used because pre-condition for all method is $True$ by default.
%Por alguna causa desconocida el metodo no funciona correctamente.
Suppose that the developer has written a program P in which uses the $swap$ method. 
For some reason the $swap$ method does not work correctly.
%El algoritmo definido en  ref debería encontrar un atajo sin utilizar el método swap. El atajo debera verificar el contrato del método swap.
The algorithm defined in \ref{propuesta} should find a PWa without using the $swap$ method. The workaround should verifies 
the $swap$ method contract.\\
The algorithm defined in \ref{propuesta} is implmented in a script Python. 
The sequence of steps is: 
\begin{enumerate}
 \item Use the Taco tool for traslate the OrderedPair.java class to a dynalloy model OrderedPair.dals. 
\\
 \item We edit the OrderedPair.dals file and adding a formula for to build new programs not deterministically. 
These programs(workaround) will not contain to the method swap (line 7 of algorithm in \ref{propuesta}). 
\\
\item The script calls the Dynalloy CITA to find a Wac. 

\item The script call to Alloy tool for checks whether the Wac is a Pwa.

This whole process is repeated until a Pwa found or until it exceeds the Wac to search.\\

Notice: we make an abstraction of such methods to add the model Dynalloy(figure CITA).  
\\
\\
\\
\begin{center}
\begin{tabular}{| l | c |}
\hline
 \textbf{Sentences} & \textbf{Actions}\\
\hline
 $this.setx(getx())$ & $setx\_x$\\
\hline
 $this.setx(gety())$ & $setx\_y$\\
\hline
 $this.setx(getoldx())$ & $setx\_oldx$\\
\hline
 $this.setx(getoldy())$ & $setx\_oldy$\\
\hline
 $this.sety(gety())$ & $sety\_y$\\
\hline
 $this.sety(getx())$ & $sety\_x$\\
\hline
 $this.sety(getoldx())$ & $sety\_oldx$\\
\hline
 $this.sety(getoldy())$ & $sety\_oldy$\\
\hline
 $this.setoldx(gety())$ & $setoldx\_y$\\
\hline
 $this.setoldx(getx())$ & $setoldx\_x$\\
\hline
 $this.setoldx(getoldx())$ & $setoldx\_oldx$\\
\hline
 $this.setoldx(getoldy())$ & $setoldx\_oldy$\\
\hline
 $this.setoldy(gety())$ & $setoldy\_y$\\
\hline
 $this.setoldy(getx())$ & $setoldy\_x$\\
\hline
 $this.setoldy(getoldx())$ & $setoldy\_oldx$\\
\hline
 $this.setoldy(getoldy())$ & $setoldy\_oldy$\\
\hline
\end{tabular}\end{center}


First, we ran the python script.The script output was at first a Wac list where not contains a Pwa. This was because the contract
 allowed executions equivalent to skip. For example, the trace:  \\
\begin{center}
${setoldx_y setoldx_y setoldy_x setoldy_x setoldy_x}$                                                     
\end{center}

This trace produces no change in the values ​​of x and y. 
For the current contract $swap$ method, the trace is equivalent to running skip action.
To remove these traces, we made the stronger the swap contract method. The new contract is: 

\begin{center}
\begin{verbatim}
/*@
  @ ensures x == \old(y);
  @ ensures y == \old(x);
  @ ensures x != \old(x);
  @ ensures y != \old(y);
  @*/
\end{verbatim}\end{center}

The postcondition requires not only the values ​​of $x$ and $y$ are exchanged, but also the old values ​​of $x$ and 
$y$ are diferenes to the final values ​​of $x$ and $y$. With this new contract, we ran the script 
again and we find the following Pwa: 
\\
\begin{center}
${ sety_oldy setx_y sety_oldy sety_oldy sety_oldx}$                                                     
\end{center}

\end{enumerate}


 





 








